public class HashTable {
    //TODO clean
	/*@ spec_public nullable @*/ EntryList[] arr; 
	/*@ spec_public @*/ int size;
	
	
	//@ invariant arr !=null;
	//@ invariant size >= 0;  
	
	// removed this && size < arr.length; don't think we need that.. 
	
	/*@ invariant (\forall Object x; this.contains(x);
	  @ arr[(Math.abs(x.hashCode())%arr.length)].contains(x));
	  @*/
	
	/*@ invariant size == 
	  @ (\max int n; n >= 0 && (\exists Object x; this.contains(x)); n + 1); 
	  @*/

    /* A simple linked list of entries. */
    private class EntryList {
    	
    	/*@ spec_public non_null @*/ Object first;
    	/*@ spec_public nullable @*/ EntryList rest;
    		
    	/*@ invariant (\forall Object x; this.contains(x) && rest != null; 
    	  @ !rest.contains(x) ==> first.equals(x));
	 	  @*/

      	EntryList( Object first, EntryList rest ) {
	        this.first = first;
      	    this.rest = rest;
       	}
      	
      	/*@ public normal_behavior
      	  @ requires o == null;
      	  @ ensures \result == false;
      	  @ also
      	  @ requires first.equals(o);
      	  @ ensures \result == true;
      	  @ also
      	  @ requires rest != null;
      	  @ ensures \result ==  true ==> rest.contains(o);
      	  @*/
      	// The second result could be like this as well 
      	// (\exists Object first; first.equals(o));
      	
      	/*@ pure @*/
      	@SuppressWarnings("unused")
		boolean contains(Object o) {
      		 if (o == null) {
                 return false; 
      		 }
             return (first.equals(o) || (rest != null &&  rest.contains(o)));
      	}
    }
    
    /* Creates an empty hashtable with an array of length init.
     */
    public HashTable( int init ) {
    		arr = new EntryList[init];
    		size = 0;
    }

    /* Returns the size.
     */

    // Old size return apparently wrong?
  
    
    /*//////////////// 2012-12-04 ////////////////////
     * You have to say that size is the number of element contained in the 
     * hashtable. This should be an invariant.
	 *	-gapag
	 * The problem is the absence of an invariant for the size, other than what
	 * we have I assume... 
     */

    
    /*@ public normal_behavior
    @ 
    @ ensures \result == size;
    @*/
    
    public int getSize() {
		return size;
    }

    /* Adds x to the hashtable
     */
   /*@ public normal_behavior
     @ requires x == null;
     @ ensures size == \old(size);
     @ ensures (\forall Object e; \old(this).contains(e) <==> this.contains(e));
     @ assignable \nothing;
     @ also
     @ requires x != null;
     @ ensures \old(contains(x)) ==> size == \old(size);
     @ ensures \old(!contains(x)) ==> size == \old(size)+1;
     @ ensures (\forall Object e; !e.equals(x);
     @     \old(this).contains(e) <==> this.contains(e));
     @ assignable arr;
     @ assignable size;
     @*/
    public void add( Object x ) {
    
		    int ix = Math.abs(x.hashCode() % arr.length);
    		EntryList entLi = arr[ix];
	
		    if ( entLi != null ) {
		        while ( entLi.rest != null ) {
		        		if ( entLi.first.equals( x ) )
		        		    return;
        				entLi = entLi.rest;
		        }

      	    entLi.rest = new EntryList(x,null);
	      }
	      else
	          arr[ix] = new EntryList(x,null);
	          
	    	size++;
    }
    
    /* Checks if x is in the hashtable.
     */
   /*@ public normal_behavior
     @ requires x==null;
     @ ensures \result == false;
     @ also
     @ requires x!=null;
     @ ensures \result == (arr[x.hashCode() % arr.length].contains(x));
     @*/
    
    public boolean contains( Object x ) {

		    int ix = Math.abs(x.hashCode()) % arr.length;
	
		    for ( EntryList entLi = arr[ix]; entLi != null; entLi = entLi.rest )
		        if ( entLi.first.equals( x ) )
		          	return true;
		    
		    return false; 
		    
    }
    
    /* Removes x from the hashtable.
     */
    
  /*@ public normal_behavior 
    @ requires x == null;
    @ ensures size == \old(size);
    @ ensures (\forall Object e; \old(this).contains(e) <==> this.contains(e));
    @ assignable \nothing;
    @ 
    @ also
    @ 
    @ requires x != null;
    @ ensures \old(contains(x)) ==> size == \old(size)+1;
    @ ensures \old(!contains(x)) ==> size == \old(size);
    @ ensures (\forall Object e; !e.equals(x);
    @     \old(this).contains(e) <==> this.contains(e));
    @ ensures !contains(x);
    @*/
    
    public void remove( Object x ) {
	
    		int ix = Math.abs(x.hashCode() % arr.length);
    		EntryList entLi = arr[ix];
	
    		if ( entLi != null ) {
		        while ( entLi.rest != null ) {
		        		if ( entLi.rest.first.equals( x ) ) {
		        		    entLi.rest = entLi.rest.rest;
		        		    size--;
		        		    return;
        				}
      		    	entLi = entLi.rest;
     		    }
		    }
    }
  
}

